| Model: | ftwc v.3 (MA) |
| Parameter(s) | N = 8, TIME_BOUND = 5 |
| Property: | TimeMax (exp-time) |
~/storm/build/bin/storm --jani ftwc.jani --janiproperty TimeMax --constants N=8,TIME_BOUND=5 --timebounded:precision 1e-3 --engine portfolio --ddlib sylvan --sylvan:maxmem 6114 --sylvan:threads 4
| Walltime: | 11.646022319793701s |
| Return code: | 0 |
| Note(s): | The tool result '936814393/500' is tagged as incorrect. The reference result is '14147539327715842970938081149439827556191855684986157225275420283904447111639173866985598067681880129145471955175837520484728674160947632314097414522215685810225289457464569207661091813307674297797143727174955440899483387407321681291184424506984992879012095530345285342024382474295791214853480384950324618438986141022393122221483515220059469437753580148566940023111369720706495584592910594485865392023065207484361584743733034472966492554451495384839780894386232463996592241438310525820998238718273578495918691672707401317176748184096327147856287264972471729588120240871838813879102585106207566691951399630379924021184728534349249967428450718614502037376678686402345692320311432491400624417178668317054297945120230434734671616812283656994600039357609515482255775387934878545716862747289920261364983342431626411334568200844878035785326549818269149287216092984331688654368905681236451815235937234883596128115298847189295790398147570144922809063167063962528551290722287316226930957361364621078617332124555611429900248705271716919382952114182769664485935394801970185448606996794475223351459359903585908150996048008741267160553266728914830252425526888638356128136225965167103122471272719550780556236642932222129696893467798030685193910202459950136951210238061689767579289643629303538542482870365261684890789158469324399903966074520435527400513184215701818535283932228822505417379643982708346744529249186030685601025189583144333201907054210070389572822374379524345297468243673733681004505816067531925822483031159282502142162128798124696802883448494004237017224443773454288483864754258272527830640/7089094486886152998759701300155500901998069494141378595082824220245193350841445442005921773373232468017404127046556816066172763832380898910759166783537122001803327415928789825044733438472368045971841355042333453313408686801655334985604705662488624072106433169111514928011691630773128060762623647992193034103190205909522064284047406323039604970403662201093284654054668452958183491297234244286068372763681370374726266308384622991328027205137693205600349183630125185371154573438258533712673412092877867700804884242902932346745349737176013215024325934627692482375927103941857100787490885917030247827459468997131837311668119854984798438962147706033548207098166939858066166831031219780220860594464147951283203961313594611332813759008724366176890429238998756081269324185116147876631957504095092112063260715169869160852842053825386369654224518690209505776178114050426878639030562327723451225362726314274693283245586900228586107330822034570017057331353785903279175727640306095100457629735940432349260334397741951039453474516789481757111542043748817172460259862875923592130952148356005729896464017339356784874328772912970518594071618611390735874646725183844220406819689970562199385068078117100272085488538668067127129148217908112211166685047613169246816871377941639068555593821218761881242401764378919825272403279105173337534011696735068919735562378509544701365166973746868641592503726967758543209499093761767328716973178924345448469760039826975572631209478350903760987830627909300587633645379160137966039250297375844157563695341953903748513131242807046379927336025645261638001926334008796169' (approx. 1995676.5076113513) which means a relative error of '0.06115606469579168' which is larger than the goal precision '0.001'. |
| Relative Error: | 0.06115606469579168 |
Storm 1.5.1 Date: Wed Mar 18 23:40:00 2020 Command line arguments: --jani ftwc.jani --janiproperty TimeMax --constants 'N=8,TIME_BOUND=5' '--timebounded:precision' 1e-3 --engine portfolio --ddlib sylvan '--sylvan:maxmem' 6114 '--sylvan:threads' 4 Current working directory: / Time for model input parsing: 0.003s. Portfolio engine picked the following settings: engine=sparse bisimulation=false exact=false Time for model construction: 0.097s. -------------------------------------------------------------- Model type: Markov Automaton (sparse) States: 10299 Transitions: 26983 Choices: 12635 Markovian St.: 4951 Max. Rate.: 2.0307 Reward Models: none State Labels: 3 labels * deadlock -> 0 item(s) * (((workstations_up[0] = 0) | switches_down[0]) & ((workstations_up[1] = 0) | switches_down[1])) -> 1059 item(s) * init -> 1 item(s) Choice Labels: none -------------------------------------------------------------- Time for model preprocessing: 0.000s. -------------------------------------------------------------- Model type: Markov Automaton (sparse) States: 10299 Transitions: 26983 Choices: 12635 Markovian St.: 4951 Max. Rate.: 2.0307 Reward Models: none State Labels: 3 labels * deadlock -> 0 item(s) * (((workstations_up[0] = 0) | switches_down[0]) & ((workstations_up[1] = 0) | switches_down[1])) -> 1059 item(s) * init -> 1 item(s) Choice Labels: none -------------------------------------------------------------- Model checking property "TimeMax": T[exp]max=? [F (((workstations_up[0] = 0) | switches_down[0]) & ((workstations_up[1] = 0) | switches_down[1]))] ... Result (for initial states): 1873628.786 Time for model checking: 11.514s.